{-# LANGUAGE TypeFamilies, TemplateHaskell, FlexibleInstances,
  FlexibleContexts, UndecidableInstances, GADTs, MultiParamTypeClasses,
  TypeOperators, NoImplicitPrelude, EmptyDataDecls #-}

{-# OPTIONS_GHC -fcontext-stack=250 #-}

module Data.Yoko.Reflect.Prelude where

import Type.Serialize (encode)

import Data.Yoko hiding (Just, Nothing)

import Prelude hiding (Maybe(..), Either(..))
import qualified Prelude
import Prelude (Maybe, Either)




data Unit

concat `fmap` mapM derive [''(), ''Unit]

type instance Tag Unit = $(return $ encode "Unit")
type instance Range Unit = ()
instance DC Unit where
  occName _ = "()"
  fr _ = ()
data instance RM m (N Unit) = Unit
type instance Rep Unit = U
instance Generic Unit where rep _ = U; obj _ = Unit

type instance DTs () = UnitDTs
data instance DCs () dc where Unit_ :: DCs () Unit
instance DT () where
  packageName _ = "yoko"
  moduleName _ = "Data.Yoko.Reflect"
  disband _ = disbanded Unit
type instance Fin (DCs ()) = (:=:) Unit
instance Finite (DCs ()) where toFin Unit_ = membership; predFin _ _ x = x
instance Etinif (DCs ()) where frFin Refl = Unit_

data UnitDTs t where Unit__ :: UnitDTs ()
type instance Fin UnitDTs = (:=:) ()
instance Finite UnitDTs where toFin Unit__ = Refl; predFin _ _ x = x
instance Etinif UnitDTs where frFin Refl = Unit__

finite_set [t|UnitDTs|]





data Nil a
type instance Tag (Nil a) = $(return $ encode "[]")
type instance Rep (Nil a) = U
data instance RM m (N (Nil a)) = Nil 
instance Generic (Nil a) where rep _ = U; obj _ = Nil
type instance Range (Nil a) = [a]
instance (EQ ~ Compare a a) => DC (Nil a) where
  occName _ = "[]"
  fr _ = []

data Cons a
type instance Tag (Cons a) = $(return $ encode ":")
type instance Rep (Cons a) = D a :* R [a] :* U
data instance RM m (N (Cons a)) = Cons a (Med m [a])
instance Generic (Cons a) where
  rep ~(Cons a x) = D a :* R x :* U
  obj ~(D a :* R x :* U) = Cons a x
type instance Range (Cons a) = [a]
instance (EQ ~ Compare a a) => DC (Cons a) where
  occName _ = ":"
  fr ~(Cons a x) = a : x

type instance DTs [a] = ListDTs a
data instance DCs [a] dc where Cons_ :: DCs [a] (Cons a); Nil_ :: DCs [a] (Nil a)
instance (EQ ~ Compare a a) => DT [a] where
  packageName _ = "yoko"
  moduleName _ = "Examples.Prelude"
  disband (a : x) = disbanded $ Cons a x
  disband [] = disbanded Nil
type instance Fin (DCs [a]) = (:=:) (Nil a) :|| (:=:) (Cons a)
instance Finite (DCs [a]) where
  toFin Nil_ = LeftU Refl
  toFin Cons_ = RightU Refl
  predFin _ _ x = x
instance Etinif (DCs [a]) where
  frFin (LeftU  Refl) = Nil_
  frFin (RightU Refl) = Cons_

data ListDTs a t where List__ :: ListDTs a [a]
type instance Fin (ListDTs a) = (:=:) [a]
instance Finite (ListDTs a) where toFin List__ = Refl; predFin _ _ x = x
instance Etinif (ListDTs a) where frFin Refl = List__

instance (EQ ~ Compare a a) => SetModel (ListDTs a) where
  evidence List__ x = x
instance (a ~ b, EQ ~ Compare a a) => [a] ::: ListDTs b where membership = List__
type instance t ::? ListDTs a = t ::? Fin (ListDTs a)
instance EqT (ListDTs a) where eqT = eqTFin
instance ([a] ::: v) => ListDTs a :=> v where weaken = weakenFin

concat `fmap` mapM derive [''[], ''Cons, ''Nil]





data Nothing a
type instance Tag (Nothing a) = $(return $ encode "Nothing")
type instance Rep (Nothing a) = U
data instance RM m (N (Nothing a)) = Nothing 
instance Generic (Nothing a) where rep _ = U; obj _ = Nothing
type instance Range (Nothing a) = Maybe a
instance (EQ ~ Compare a a) => DC (Nothing a) where
  occName _ = "Nothing"
  fr _ = Prelude.Nothing

data Just a
type instance Tag (Just a) = $(return $ encode "Just")
type instance Rep (Just a) = D a :* U
data instance RM m (N (Just a)) = Just a
instance Generic (Just a) where
  rep ~(Just a) = D a :* U
  obj ~(D a :* U) = Just a
type instance Range (Just a) = Maybe a
instance (EQ ~ Compare a a) => DC (Just a) where
  occName _ = "Just"
  fr ~(Just a) = Prelude.Just a

type instance DTs (Maybe a) = MaybeDTs a
data instance DCs (Maybe a) dc where
  Just_ :: DCs (Maybe a) (Just a)
  Nothing_ :: DCs (Maybe a) (Nothing a)
instance (EQ ~ Compare a a) => DT (Maybe a) where
  packageName _ = "yoko"
  moduleName _ = "Examples.Prelude"
  disband (Prelude.Just a) = disbanded $ Just a
  disband Prelude.Nothing = disbanded Nothing
type instance Fin (DCs (Maybe a)) = (:=:) (Nothing a) :|| (:=:) (Just a)
instance Finite (DCs (Maybe a)) where
  toFin Nothing_ = LeftU Refl
  toFin Just_ = RightU Refl
  predFin _ _ x = x
instance Etinif (DCs (Maybe a)) where
  frFin (LeftU  Refl) = Nothing_
  frFin (RightU Refl) = Just_

data MaybeDTs a t where Maybe__ :: MaybeDTs a (Maybe a)
type instance Fin (MaybeDTs a) = (:=:) (Maybe a)
instance Finite (MaybeDTs a) where toFin Maybe__ = Refl; predFin _ _ x = x
instance Etinif (MaybeDTs a) where frFin Refl = Maybe__

instance (EQ ~ Compare a a) => SetModel (MaybeDTs a) where
  evidence Maybe__ x = x
instance (a ~ b, EQ ~ Compare a a) => (Maybe a) ::: MaybeDTs b where membership = Maybe__
type instance t ::? MaybeDTs a = t ::? Fin (MaybeDTs a)
instance EqT (MaybeDTs a) where eqT = eqTFin
instance (Maybe a ::: v) => MaybeDTs a :=> v where weaken = weakenFin

concat `fmap` mapM derive [''Maybe, ''Just, ''Nothing]





data Left a b
type instance Tag (Left a b) = $(return $ encode "Left")
type instance Rep (Left a b) = D a :* U
data instance RM m (N (Left a b)) = Left a
instance Generic (Left a b) where
  rep (Left a) = D a :* U 
  obj (D a :* U) = Left a 
type instance Range (Left a b) = Either a b
instance (EQ ~ Compare a a, EQ ~ Compare b b) => DC (Left a b) where
  occName _ = "Left"
  fr (Left a) = Prelude.Left a

data Right a b
type instance Tag (Right a b) = $(return $ encode "Right")
type instance Rep (Right a b) = D b :* U
data instance RM m (N (Right a b)) = Right b
instance Generic (Right a b) where
  rep ~(Right b) = D b :* U
  obj ~(D b :* U) = Right b
type instance Range (Right a b) = Either a b
instance (EQ ~ Compare a a, EQ ~ Compare b b) => DC (Right a b) where
  occName _ = "Right"
  fr ~(Right b) = Prelude.Right b

type instance DTs (Either a b) = EitherDTs a b
data instance DCs (Either a b) dc where
  Left_ :: DCs (Either a b) (Left a b)
  Right_ :: DCs (Either a b) (Right a b)
instance (EQ ~ Compare a a, EQ ~ Compare b b) => DT (Either a b) where
  packageName _ = "yoko"
  moduleName _ = "Examples.Prelude"
  disband (Prelude.Right b) = disbanded $ Right b
  disband (Prelude.Left a) = disbanded $ Left a
type instance Fin (DCs (Either a b)) = (:=:) (Left a b) :|| (:=:) (Right a b)
instance Finite (DCs (Either a b)) where
  toFin Left_ = LeftU Refl
  toFin Right_ = RightU Refl
  predFin _ _ x = x
instance Etinif (DCs (Either a b)) where
  frFin (LeftU  Refl) = Left_
  frFin (RightU Refl) = Right_

data EitherDTs a b t where Either__ :: EitherDTs a b (Either a b)
type instance Fin (EitherDTs a b) = (:=:) (Either a b)
instance Finite (EitherDTs a b) where toFin Either__ = Refl; predFin _ _ x = x
instance Etinif (EitherDTs a b) where frFin Refl = Either__

instance (EQ ~ Compare a a, EQ ~ Compare b b) => SetModel (EitherDTs a b) where
  evidence Either__ x = x
instance (a ~ c, b ~ d, EQ ~ Compare a a, EQ ~ Compare b b
         ) => (Either a b) ::: EitherDTs c d where membership = Either__
type instance t ::? EitherDTs a b = t ::? Fin (EitherDTs a b)
instance EqT (EitherDTs a b) where eqT = eqTFin
instance (Either a b ::: v) => EitherDTs a b :=> v where weaken = weakenFin

concat `fmap` mapM derive [''Either, ''Right, ''Left]
